Require Import AutoSep.

Definition swapS := SPEC("x", "y") reserving 2
  Ex v, Ex w,
  PRE[V] V "x" =*> v * V "y" =*> w
  POST[_] V "x" =*> w * V "y" =*> v.

Definition swap := bmodule "swap" {{
  bfunction "swap"("x", "y", "v", "w") [swapS]
    "v" <-* "x";;
    "w" <-* "y";;
    "x" *<- "w";;
    "y" *<- "v";;
    Return 0
  end
}}.

Theorem swapOk : moduleOk swap.
Proof.
  vcgen; sep_auto.
Qed.

Definition two_way_sortS := SPEC("a", "len") reserving 8
  PRE[_] [| True |] 
  POST[_] [| True |].

Definition two_way_sort := bimport [[ "swap"!"swap" @ [swapS] ]]
bmodule "two_way_sort" {{
  bfunction "two_way_sort"("a", "len", "i", "j", "t") [two_way_sortS]
    "i" <- "a";;
    "j" <- "len" * 4;;
    "j" <- "a" + "j";;
    "j" <- "j" - 4;;
    [PRE[_] [| True |]
      POST[_] [| True |]
    ]
    While ("i" <= "j") {
      "t" <-* "i";;
      If ("t" = 0) {
        "i" <- "i" + 4
      } else {
        "t" <-* "j";;
        If ("t" <> 0) {
          "j" <- "j" - 4
        } else {
          Call "swap"!"swap"("i", "j")[
            PRE[_] [| True |]
            POST[_] [| True |]
          ];;
          "i" <- "i" + 4;;
          "j" <- "j" - 4
        }
      }
    };;
    Return "a"
  end
}}.

Theorem two_way_sortOK : moduleOk two_way_sort.
Proof.
  vcgen.
  post.
  post.
  evaluate auto_ext.
  post.
  evaluate auto_ext.
  descend.
  step auto_ext.
  step auto_ext.
  Focus 1.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  Focus 1.
  post.
  evaluate auto_ext.
  Focus 1.
  post.
  evaluate auto_ext.
  descend.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  Focus 1.
  post.
  evaluate auto_ext.
  Focus 1.
  post.
  Focus 1.
  descend.
  Focus 1.
  
 